(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const r7 Real)
(declare-const v4 Bool)
(assert v1)
(declare-const v5 Bool)
(assert v5)
(declare-const v6 Bool)
(assert v2)
(declare-const v7 Bool)
(declare-const r8 Real)
(assert (or (= r2 r2 9646.29 r2 r3) (<= 94039474 3 r2 94039474 r2) (= v2 v2 v1 v1 v3 v3) (>= r7 2180030 r2) (< 2180030 9646.29) v7))
(assert (xor v3 (= v2 v2 v1 v1 v3 v3) (= 298128772 r7 (- 94039474) 298128772 9646.29) (= v2 v2 v1 v1 v3 v3) (>= r7 2180030 r2) v6 v2 (and v1 v2 (distinct v2 v3 v4 v3 (= v2 v2 v1 v1 v3 v3) (= v2 v2 v1 v1 v3 v3)) v3 v3 v4 v1 (= v2 v2 v1 v1 v3 v3) (not v4) v1 (distinct v2 v3 v4 v3 (= v2 v2 v1 v1 v3 v3) (= v2 v2 v1 v1 v3 v3))) v5 (xor v5 (>= r7 2180030 r2) (>= r7 2180030 r2) (< 2180030 9646.29) v0) (distinct v2 v3 v4 v3 (= v2 v2 v1 v1 v3 v3) (= v2 v2 v1 v1 v3 v3))))
(assert (= (or (and v1 v2 (distinct v2 v3 v4 v3 (= v2 v2 v1 v1 v3 v3) (= v2 v2 v1 v1 v3 v3)) v3 v3 v4 v1 (= v2 v2 v1 v1 v3 v3) (not v4) v1 (distinct v2 v3 v4 v3 (= v2 v2 v1 v1 v3 v3) (= v2 v2 v1 v1 v3 v3))) (= v2 v2 v1 v1 v3 v3) v3 v3) (= v2 v2 v1 v1 v3 v3)))
(declare-const v8 Bool)
(declare-const r9 Real)
(assert (=> v3 (or (and v1 v2 (distinct v2 v3 v4 v3 (= v2 v2 v1 v1 v3 v3) (= v2 v2 v1 v1 v3 v3)) v3 v3 v4 v1 (= v2 v2 v1 v1 v3 v3) (not v4) v1 (distinct v2 v3 v4 v3 (= v2 v2 v1 v1 v3 v3) (= v2 v2 v1 v1 v3 v3))) (= v2 v2 v1 v1 v3 v3) v3 v3)))
(check-sat)
